Search for: All records

Two new compounds, Zn2FeSbO6 and Zn2MnSbO6, have been synthesized under high-pressure and high-temperature conditions. The synthesis, single-crystal and powder X-ray diffraction, X-ray absorption near-edge spectroscopy (XANES), optical second harmonic generation (SHG), and magnetic and heat capacity measurements were carried out for both compounds and are described. The lattice parameters are a = 5.17754(6) Å and c = 13.80045(16) Å for Zn2FeSbO6 and a = 5.1889(10) Å and c = 14.0418(3) Å for Zn2MnSbO6. Single-crystal X-ray diffraction analyses indicate that Zn2FeSbO6 consists of a cocrystal of superimposed Ni3TeO6 (NTO) and ordered ilmenite (OIL) components with a ratio of approximately 2:1 and Zn2MnSbO6 contains two nearly identical, but noncrystallographically related, OIL components in a ratio of approximately 6:1. 

Relational network verification is a new approach for validating network changes. In contrast to traditional network verification, which analyzes specifications for a single network snapshot, it analyzes specifications that capture similarities and differences between two network snapshots (e.g., pre- and post-change snapshots). Relational specifications are compact and precise because they focus on the flows and paths that change between snapshots and then simply mandate that all other network behaviors "stay the same", without enumerating them. To achieve similar guarantees, single-snapshot specifications would need to enumerate all flow and path behaviors that are not expected to change in order to enable checking that nothing has accidentally changed. Such specifications are proportional to network size, which makes them impractical to generate for many real-world networks. We demonstrate the value of relational reasoning by developing Rela, a high-level relational specification language and verification tool for network changes. Rela compiles input specifications and network snapshot representations to finite state automata, and it then verifies compliance by checking automaton equivalence. Our experiments using data from a global backbone with over 103 routers find that Rela specifications need fewer than 10 terms for 93% of the complex, high-risk changes. Rela validates 80% of the changes within 20 minutes. 

Satisfiability Modulo Theories (SMT)-based analysis allows exhaustive reasoning over complex distributed control plane routing behaviors, enabling verification of converged routing states under arbitrary conditions. To improve scalability of SMT solving, we introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments. Users specify an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using these annotations to define assumptions and guarantees over fragments akin to assume-guarantee reasoning. We prove that any converged states of the fragments are converged states of the monolithic network, and there exists an annotated cut that can generate fragments corresponding to any converged state of the monolithic network. We implement this procedure as Kirigami, an extension of the network verification language and tool NV, and evaluate it on industrial topologies with synthesized policies. We observe a 10x improvement in end-to-end NV verification time, with SMT solve time improving by up to 6 orders of magnitude. 

We develop FLM, a high-level language that enables network operators to write programs that recognize and react to specific packet sequences. To be able to examine every packet, our compilation procedure can transform FLM programs into P4 code that can run on programmable switch ASICs. It first splits FLM programs into a state management component and a classical regular expression, then generates an efficient implementation of the regular expression using SMT-based program synthesis. Our experiments find that FLM can express 15 sequence monitoring tasks drawn from prior literature. Our compiler can convert all of these programs to run on switch hardware in way that fit within available pipeline stages and consume less than 15% additional header fields and instruction words when run alongside switch programs. 

The development of programmable switches such as the Intel Tofino has allowed network designers to implement a wide range of new in-network applications and network control logic. However, current switch programming languages, like P4, operate at a very low level of abstraction. This paper introduces SwitchLog, a new experimental logic programming language designed to lift the level of abstraction at which network programmers operate, while remaining amenable to efficient implementation on programmable switches. SwitchLog is inspired by previous distributed logic programming languages such as NDLog, in which programmers declare a series of facts, each located at a particular switch in the network. Logic programming rules that operate on facts at different locations implicitly generate network communication, and are updated incrementally, as packets pass through a switch. In order to ensure these updates can be implemented efficiently on switch hardware, SwitchLog imposes several restrictions on the way programmers can craft their rules. We demonstrate that SwitchLog can be used to express a variety of networking applications in a mere handful of lines of code. 

Influenza viruses are a major global health burden with up to 650,000 associated deaths annually. Beyond seasonal illness, influenza A viruses (IAVs) pose a constant pandemic threat due to novel emergent viruses that have evolved the ability to jump from their natural avian hosts to humans. Because of this threat, active surveillance of circulating IAV strains in wild and domestic bird populations is vital to our pandemic preparedness and response strategies. Here, we report on IAV surveillance data collected from 2017 to 2022 from wild and domestic birds in Bangladesh. We note evidence to suggest that male birds show a higher risk of IAV, including highly pathogenic avian influenza (HPAI) A(H5) virus, positivity than female birds. The data was stratified to control for selection bias and confounding variables to test the hypothesis that male birds are at a higher risk of IAV positivity relative to female birds. The association of IAV and A(H5) largely held in each stratum, and double stratification suggested that the phenomena was largely specific to ducks. Finally, we show that chickens, male birds, and juvenile birds generally have higher viral loads compared to their counterparts. These observations warrant further validation through active surveillance across various populations. Such efforts could significantly contribute to the enhancement of pandemic prediction and risk assessment models.